i:Id, ds:x:Id fp Type, x:Id, k:Knd, T:Type, test:(State(ds)T).
((x  dom(ds)))
 ((isrcv(k))  (i = destination(lnk(k))))
 Normal(T)
 Normal(ds)
 R-base-recognize(i;ds;x;k;T;test)
 ||- es.(@i(x:) & (state@i r State(ds)) & (kindtype(i;k) r T))
 ||- es.c e@i.
 ||- es.c ((x when e))
 ||- es.c  (e':E
 ||- es.c  ((((e' <loc e) & kind(e') = k  Knd) c ((test((state when e'),val(e')))))) 

latex

Definitions

if b then t else f fi , P  Q, ff, x:A. B(x), P  Q, b, Top, {T}, SQType(T), x. t(x), , t  T, e@i. P(e), P & Q, A c B, R ||- es.P(es), P  Q, x:A. B(x), False, (e <loc e'), @i(x:T), A, P  Q, Dec(P), x(s), recognizer(es;i;ds;x;k;T;test)

Lemmas

es-le wf, es-le-pred, es-le-loc, es-locl wf, es-locl transitivity1, es-pred-locl, es-after-pred2, es-after wf, es-pred wf, es-locl-iff, es-loc-pred, false wf, es-dtype wf, es-when-first-discrete, es-vartype wf, es-when wf, bool sq, es-first wf, decidable assert, es-kind wf, Knd sq, es-valtype-kindtype, es-E wf, es-loc wf, Id sq, es-state-when wf, fpf wf, Knd wf, bool wf, decl-state wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, not wf, lnk wf, ldst wf, Id wf, isrcv wf, assert wf, normal-type wf, normal-ds wf, event system wf, R-base-recognize wf, R-consistent wf, R-base-recognize-realizes2